Library complement
Require Export PointsType.
Require Import PointsETC.
Require Import TrianglesDefs.
Require Import incidence.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition complement P :=
match P with
cTriple p q r ⇒
cTriple ((b×q+c×r)/a) ((a×p+c×r)/b) ((a×p+b×q)/c)
end.
Definition anticomplement P :=
match P with
cTriple p q r ⇒
cTriple ((-a×p+b×q+c×r)/a) ((a×p-b×q+c×r)/b) ((a×p+b×q-c×r)/c)
end.
Require Import PointsETC.
Require Import TrianglesDefs.
Require Import incidence.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition complement P :=
match P with
cTriple p q r ⇒
cTriple ((b×q+c×r)/a) ((a×p+c×r)/b) ((a×p+b×q)/c)
end.
Definition anticomplement P :=
match P with
cTriple p q r ⇒
cTriple ((-a×p+b×q+c×r)/a) ((a×p-b×q+c×r)/b) ((a×p+b×q-c×r)/c)
end.
The complement of a point P is on the line PG where G is the centroid (X_2).
Lemma complement_property :
∀ P,
col P (complement P) X_2.
Proof.
intros.
destruct P.
unfold col, complement, X_2.
simpl.
field.
split;
auto with triangle_hyps.
Qed.
The anti-complement of a point P is on the line PG where G is the centroid (X_2).
Lemma anticomplement_property :
∀ P,
col P (anticomplement P) X_2.
Proof.
intros.
destruct P.
unfold col. simpl.
field.
split;
auto with triangle_hyps.
Qed.
Lemma anticomplement_complement_property :
∀ P,
eq_points (anticomplement (complement P)) P.
Proof.
destruct P.
unfold eq_points. simpl.
split;field;auto with triangle_hyps.
Qed.
Lemma complement_anticomplement_property :
∀ P,
eq_points (complement (anticomplement P)) P.
Proof.
destruct P.
unfold eq_points. simpl.
split;field;auto with triangle_hyps.
Qed.
Lemma medial_triangle_is_complement_triangle_of_ABC :
eq_triangles medial_triangle (complement pointA, complement pointB, complement pointC).
Proof.
unfold medial_triangle.
red;
simpl.
unfold eq_points.
simpl.
repeat split;field;auto with triangle_hyps.
Qed.
Lemma X_74_complement_X_146 :
eq_points X_74 (complement X_146).
Proof.
intros.
red.
simpl.
unfold SA, SB, SC.
split;field;auto with triangle_hyps.
Qed.
End Triangle.